| Definitions |  T, P  Q, P   Q, P  Q, A c B, Rsends-T(x1), Rsends-knd(x1), Reffect-T(x1), Rsends-dt(x1), Rsends-l(x1), p  q, Reffect-knd(x1), let x = a in b(x), Reffect?(x1), Rsends?(x1), R-interface-compat(A;B), R-loc(R), R-Feasible(R), True, P & Q, Rnone?(x1), Rplus?(x1),  b, Y, reduce(f;k;as), t.1, deq-member(eq;x;L), x  dom(f),  , f(x)?z, Knd, Valtype(da;k), ff, tt,   x. t(x), if b then t else f fi , Top,  , {T}, SQType(T), R-da(R;i), i  j , False,  A, A  B, t T,  , P Q,  x:A. B(x), Rpre(loc;ds;a;p;P), Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), isl(x), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), Rsends(ds;knd;T;l;dt;g), isrcv(k), es realizer ind, Reffect(loc;ds;knd;T;x;f), Realizer, Unit,  , x(s), A || B,  , a = b, left  right, Rnone(),  |
| Lemmas | Rpre wf, or functionality wrt iff, assert of bor, bnot thru band, squash wf, bor wf, and functionality wrt iff, assert of band, lnk-decl-cap2, isrcv-implies, fpf-cap-single1, fpf-single-dom, fpf-single wf, Rsends wf, locl wf, p-outcome wf, lnk-decl wf, fpf-join wf, tagof wf, id-deq wf, assert-eq-lnk, eq lnk wf, band wf, normal-type wf, normal-ds wf, ifthenelse wf, subtype rel self, subtype rel transitivity, Knd sq, assert-eq-knd, eq knd wf, fpf-cap-single, fpf-empty wf, fpf-single wf3, subtype-top, Reffect wf, Rrframe wf, Rbframe wf, Raframe wf, Rsframe wf, Rframe wf, Rinit wf, Rplus wf, false wf, true wf, Rnone wf, R-interface-compat wf, finite-prob-space wf, decl-type wf, decl-state wf, rationals wf, unit wf, Rda wf, subtype-fpf-cap5, R-da-Rda, not functionality wrt iff, assert-eq-id, R-loc wf, eq id wf, Id wf, IdLnk wf, fpf-cap wf, ma-valtype wf, Rnone-implies, Rnone? wf, ldst wf, fpf-dom wf, Rplus-right wf, top wf, fpf wf, fpf-trivial-subtype-top, lnk wf, lsrc wf, Rplus-left wf, R-da wf, Kind-deq wf, fpf-join-cap-sq, R-size-decreases, R-Feasible-Rplus, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, Rplus-implies, eqtt to assert, bool wf, bool sq, Rplus? wf, bool cases, ge wf, nat properties, es realizer wf, R-Feasible wf, R-compat wf, Knd wf, isrcv wf, assert wf, le wf, nat plus wf, R-size wf, nat wf |
r Valtype(R-da(B;destination(lnk(k)));k)))